\begin{tabbing}
$p$ = $q$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=1of($p$)=$_{2}$1of($q$)\+
\\[0ex]$\wedge_{2}$ \=i\=f 1of($p$)=$_{2}$1 $\vee_{2}$ 1of($p$)=$_{2}$2 $\vee_{2}$ 1of($p$)=$_{2}$6 $\vee_{2}$ 1of($p$)=$_{2}$9$\rightarrow$ 2of($p$) = 2of($q$)\+\+
\\[0ex]; 1of($p$)=$_{2}$3$\rightarrow$ 1of(2of($p$)) = 1of(2of($q$)) $\wedge_{2}$ 2of(2of($p$)) = 2of(2of($q$))
\\[0ex]; 1of($p$)=$_{2}$4$\rightarrow$ 1of(2of($p$)) = 1of(2of($q$)) $\wedge_{2}$ 2of(2of($p$)) = 2of(2of($q$))
\\[0ex]; 1of($p$)=$_{2}$5$\rightarrow$ 1of(2of($p$)) = 1of(2of($q$)) $\wedge_{2}$ 2of(2of($p$)) = 2of(2of($q$))
\\[0ex]; 1of($p$)=$_{2}$7 $\vee_{2}$ 1of($p$)=$_{2}$8$\rightarrow$ 2of($p$) = 2of($q$)
\-\\[0ex]else true$_{2}$ fi
\-\-
\end{tabbing}